$\forall$${\it ds}$:(Id$\rightarrow$Type), ${\it da}$:(Id$\rightarrow$Knd$\rightarrow$Type), $A$:Type, $X$:Interface(${\it ds}$;${\it da}$;$A$).
\\[0ex]interface{-}inr($X$) $\in$ Interface(${\it ds}$;${\it da}$;\{$x$:Top + $A$$\mid$ $\neg$($\uparrow$isl($x$))\} )